MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems
Identifieur interne : 002674 ( Main/Exploration ); précédent : 002673; suivant : 002675MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems
Auteurs : Michael Kohlhase [États-Unis] ; Andreas Franke [Allemagne]Source :
- Journal of Symbolic Computation [ 0747-7171 ] ; 2000.
Abstract
In this article we describe the data model of the MB ase system, a web-based, distributed mathematical knowledge base. This system is a mathematical service in MathWeb that offers a universal repository of formalized mathematics where the formal representation allows semantics-based retrieval of distributed mathematical facts. We classify the data necessary to represent mathematical knowledge and analyze its structure. For the logical formulation of mathematical concepts, we propose a methodology for developing representation formalisms for mathematical knowledge bases. We propose to concretely equip knowledge bases with a hierarchy of logical systems that are linked by logic morphisms. These mappings relativize formulae and proofs and thus support translation of the knowledge to the various formats currently in use in deduction systems. On the other hand they define higher language features from simpler ones and ultimately serve as a means to found the whole knowledge base in axiomatic set theory. The viability of this approach is proven by developing a sorted record-λ -calculus with dependent sorts and labeled abstraction that is well-suited both for formalizing mathematical practice and supporting efficient inference services. This “mathematical vernacular" is an extension of a sortedλ -calculus by records, dependent record sorts and selection sorts.
Url:
DOI: 10.1006/jsco.2000.0468
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000724
- to stream Istex, to step Curation: 000576
- to stream Istex, to step Checkpoint: 001F11
- to stream Main, to step Merge: 002727
- to stream Main, to step Curation: 002674
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems</title><author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name></author><author><name sortKey="Franke, Andreas" sort="Franke, Andreas" uniqKey="Franke A" first="Andreas" last="Franke">Andreas Franke</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:0BD3673AA236B44A5B37BDCA8B6B773BDB562B3C</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1006/jsco.2000.0468</idno><idno type="url">https://api.istex.fr/document/0BD3673AA236B44A5B37BDCA8B6B773BDB562B3C/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000724</idno><idno type="wicri:Area/Istex/Curation">000576</idno><idno type="wicri:Area/Istex/Checkpoint">001F11</idno><idno type="wicri:doubleKey">0747-7171:2001:Kohlhase M:mbase:representing:knowledge</idno><idno type="wicri:Area/Main/Merge">002727</idno><idno type="wicri:Area/Main/Curation">002674</idno><idno type="wicri:Area/Main/Exploration">002674</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems</title><author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name><affiliation wicri:level="4"><country xml:lang="fr">États-Unis</country><wicri:regionArea>School of Computer Science, Carnegie Mellon University, Pittsburgh</wicri:regionArea><orgName type="university">Université Carnegie-Mellon</orgName><placeName><settlement type="city">Pittsburgh</settlement><region type="state">Pennsylvanie</region></placeName></affiliation></author><author><name sortKey="Franke, Andreas" sort="Franke, Andreas" uniqKey="Franke A" first="Andreas" last="Franke">Andreas Franke</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Informatik, Saarland University, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Symbolic Computation</title><title level="j" type="abbrev">YJSCO</title><idno type="ISSN">0747-7171</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2000">2000</date><biblScope unit="volume">32</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="365">365</biblScope><biblScope unit="page" to="402">402</biblScope></imprint><idno type="ISSN">0747-7171</idno></series><idno type="istex">0BD3673AA236B44A5B37BDCA8B6B773BDB562B3C</idno><idno type="DOI">10.1006/jsco.2000.0468</idno><idno type="PII">S0747-7171(00)90468-1</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0747-7171</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this article we describe the data model of the MB ase system, a web-based, distributed mathematical knowledge base. This system is a mathematical service in MathWeb that offers a universal repository of formalized mathematics where the formal representation allows semantics-based retrieval of distributed mathematical facts. We classify the data necessary to represent mathematical knowledge and analyze its structure. For the logical formulation of mathematical concepts, we propose a methodology for developing representation formalisms for mathematical knowledge bases. We propose to concretely equip knowledge bases with a hierarchy of logical systems that are linked by logic morphisms. These mappings relativize formulae and proofs and thus support translation of the knowledge to the various formats currently in use in deduction systems. On the other hand they define higher language features from simpler ones and ultimately serve as a means to found the whole knowledge base in axiomatic set theory. The viability of this approach is proven by developing a sorted record-λ -calculus with dependent sorts and labeled abstraction that is well-suited both for formalizing mathematical practice and supporting efficient inference services. This “mathematical vernacular" is an extension of a sortedλ -calculus by records, dependent record sorts and selection sorts.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>États-Unis</li></country><region><li>Pennsylvanie</li><li>Sarre (Land)</li></region><settlement><li>Pittsburgh</li><li>Sarrebruck</li></settlement><orgName><li>Université Carnegie-Mellon</li></orgName></list><tree><country name="États-Unis"><region name="Pennsylvanie"><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name></region></country><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Franke, Andreas" sort="Franke, Andreas" uniqKey="Franke A" first="Andreas" last="Franke">Andreas Franke</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/MozartV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002674 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002674 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Musique
|area= MozartV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:0BD3673AA236B44A5B37BDCA8B6B773BDB562B3C
|texte= MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems
}}
| This area was generated with Dilib version V0.6.20. |  |